COMMENT ⊗   VALID 00002 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	We wish to describe a `language' for describing strategies and for editing
 00007 ENDMK
⊗;
We wish to describe a `language' for describing strategies and for editing
clause lists.
The language should  at the very minimum allow rather arbitrary functions
on syntactic structure of clauses terms and literal.

It is also expandable to handle semantic characterizations.

The  legal variables are of three sorts: clauses literals and terms.
At  present each formula is to be applied to a single clause, thus there
should be exactly one `clause variable', currently named  lower case c.
Thus when we give choice strategies then formula is used as a filter on each
candidate; when we use the formulas on clause-lists in the eidting phase, they
are to be `mapcar'ed .

Literal and term variables are `real'variables  and are designated by l1,l2,l3,...
and t1,t2,t3,....

All quantifiers are implicitly relativized. E.g.
∀l1∃t2... means for every literal in the current clause there is a term in l1
such that...


PRIMITIVES:

ancestry	TR(x)
If x is clause c, then TR(x) gives the ancestry.
If x is either a literal or a term --l or t-- then TR(x) gives the structure of x.

Examples:

If x is an initial clauses then TR(x) is NIL. If x is a deduction then TR gives
a  list of the clauses appearing in the derivation tree.

length		α(x)
If x is a clause then α(x) gives the usual length--number of literals.
If x is a literal or term then α(x) gives the number of symbols which appear

Examples:

α(c)=1 is true if c is a unit-clause.

depth		∂(x)
If x is a clause, then ∂(x) gives the depth of the derivation tree.
If x is a literal or term then ∂(x) gives the depth of function-nesting.


PREDICATES:

=,<,>,≠,¬	equality,less-than,greater-than,not-equal, not
∧,∨,ε		and,or,clever membership.
[ p→e; ...]	conditionals

Examples:
∂(t1)<5 ∧TR(c)=NIL
  depth of nesting is less than 5 and clause is initial.

[α(c)=1 → ∀l1 E(_,_)εTR(l1) ; T → ∀l1 ¬ -εTR(l1)]
   If clause is unit the the predicate, E, must appear; otherwise every literal
   in c must be positive.

MATCHING:

+,-		sign of a literal
⊂,⊃		set delimiters for and-membership
⊃,⊂		set delimiters for or-membershit

Examples;
⊂2,3,4⊃εTR(c)
   Each clause 2,3,and 4 must appear in the tree of c.

⊃2,3,4⊂εTR(c)
   At least one of these clauses must appeaar.

_		matches any term
x,y,z,u,v	used to match sub-terms.

Examples:
f(_,_) matches any occurrence of the function-letter,f.

f(g(x,-),_,x) matches any occurrence of f such that f's first position is
an occurrence of g; and g's first position matches the third position of f.